1 /-
2 Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel
5 -/
6
7 import linear_algebra.basic
src └──────────────────┘
8
9 /-!
10 # Multilinear maps
11
12 We define multilinear maps as maps from `Π(i : ι), M₁ i` to `M₂` which are linear in each
13 coordinate. Here, `M₁ i` and `M₂` are modules over a ring `R`, and `ι` is an arbitrary type
14 (although some statements will require it to be a fintype). This space, denoted by
15 `multilinear_map R M₁ M₂`, inherits a module structure by pointwise addition and multiplication.
16
17 ## Main definitions
18
19 * `multilinear_map R M₁ M₂` is the space of multilinear maps from `Π(i : ι), M₁ i` to `M₂`.
20 * `f.map_smul` is the multiplicativity of the multilinear map `f` along each coordinate.
21 * `f.map_add` is the additivity of the multilinear map `f` along each coordinate.
22 * `f.map_smul_univ` expresses the multiplicativity of `f` over all coordinates at the same time,
23 writing `f (λi, c i • m i)` as `univ.prod c • f m`.
24 * `f.map_add_univ` expresses the additivity of `f` over all coordinates at the same time, writing
25 `f (m + m')` as the sum over all subsets `s` of `ι` of `f (s.piecewise m m')`.
26
27 We also register isomorphisms corresponding to currying or uncurrying variables, transforming a
28 multilinear function `f` on `n+1` variables into a linear function taking values in multilinear
29 functions in `n` variables, and into a multilinear function in `n` variables taking values in linear
30 functions. These operations are called `f.curry_left` and `f.curry_right` respectively
31 (with inverses `f.uncurry_left` and `f.uncurry_right`). These operations induce linear equivalences
32 between spaces of multilinear functions in `n+1` variables and spaces of linear functions into
33 multilinear functions in `n` variables (resp. multilinear functions in `n` variables taking values
34 in linear functions), called respectively `multilinear_curry_left_equiv` and
35 `multilinear_curry_right_equiv`.
36
37 ## Implementation notes
38
39 Expressing that a map is linear along the `i`-th coordinate when all other coordinates are fixed
40 can be done in two (equivalent) different ways:
41 * fixing a vector `m : Π(j : ι - i), M₁ j.val`, and then choosing separately the `i`-th coordinate
42 * fixing a vector `m : Πj, M₁ j`, and then modifying its `i`-th coordinate
43 The second way is more artificial as the value of `m` at `i` is not relevant, but it has the
44 advantage of avoiding subtype inclusion issues. This is the definition we use, based on
45 `function.update` that allows to change the value of `m` at `i`.
46 -/
47
48 open function fin set
49
50 universes u v v' w u'
51 variables {R : Type u} {ι : Type u'} {n : ℕ} {M : fin n.succ → Type v'} {M₁ : ι → Type v} {M₂ : Type w}
id ┴ └─┘ └───┘
src ┴ └─┘ └───┘
typ ┴ └─┘ └───┘
52 [decidable_eq ι]
id └──────────┘
src └──────────┘
typ └──────────┘
53
54 /-- Multilinear maps over the ring `R`, from `Πi, M₁ i` to `M₂` where `M₁ i` and `M₂` are modules
55 over `R`. -/
56 structure multilinear_map (R : Type u) {ι : Type u'} (M₁ : ι → Type v) (M₂ : Type w)
id └──┘ └──┘ ┴ ┴ └──┘
typ └──┘ └──┘ ┴ ┴ └──┘
57 [decidable_eq ι] [ring R] [∀i, add_comm_group (M₁ i)] [add_comm_group M₂] [∀i, module R (M₁ i)]
id └──────────┘ ┴ └──┘ ┴ ┴ └────────────┘ └┘ ┴ └────────────┘ └┘ ┴ └────┘ ┴ └┘ ┴
src └──────────┘ └──┘ └────────────┘ └────────────┘ └────┘
typ └──────────┘ ┴ └──┘ ┴ ┴ └────────────┘ └┘ ┴ └────────────┘ └┘ ┴ └────┘ ┴ └┘ ┴
doc └────┘
58 [module R M₂] :=
id └────┘ ┴ └┘
src └────┘
typ └────┘ ┴ └┘
doc └────┘
59 (to_fun : (Πi, M₁ i) → M₂)
id ┴ └┘ ┴ ┴ └┘
typ ┴ └┘ ┴ ┴ └┘
60 (add : ∀(m : Πi, M₁ i) (i : ι) (x y : M₁ i),
id ┴ ┴ └┘ ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴
61 to_fun (update m i (x + y)) = to_fun (update m i x) + to_fun (update m i y))
id └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └────┘ ┴ ┴ ┴ ┴ └────┘ └────┘ ┴ ┴ ┴
src └────┘ ┴ ┴ └────┘ ┴ └────┘
typ └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └────┘ ┴ ┴ ┴ ┴ └────┘ └────┘ ┴ ┴ ┴
doc └────┘ └────┘ └────┘
62 (smul : ∀(m : Πi, M₁ i) (i : ι) (c : R) (x : M₁ i),
id ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
63 to_fun (update m i (c • x)) = c • to_fun (update m i x))
id └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └────┘ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ └────┘
typ └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └────┘ ┴ ┴ ┴
doc └────┘ └────┘
64
65 namespace multilinear_map
66
67 section ring
68
69 variables [ring R] [∀i, add_comm_group (M i)] [∀i, add_comm_group (M₁ i)] [add_comm_group M₂]
id └──┘ ┴ └────────────┘ ┴ ┴ └────────────┘ ┴ └────────────┘
src └──┘ └────────────┘ └────────────┘ └────────────┘
typ └──┘ ┴ └────────────┘ ┴ ┴ └────────────┘ ┴ └────────────┘
70 [∀i, module R (M i)] [∀i, module R (M₁ i)] [module R M₂]
id ┴ └────┘ ┴ ┴ └────┘ ┴ └────┘
src └────┘ └────┘ └────┘
typ ┴ └────┘ ┴ ┴ └────┘ ┴ └────┘
doc └────┘ └────┘ └────┘
71 (f f' : multilinear_map R M₁ M₂)
id └─────────────┘
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
72
73 instance : has_coe_to_fun (multilinear_map R M₁ M₂) := ⟨_, to_fun⟩
id └────────────┘ └─────────────┘ ┴ └┘ └┘ └────┘
src └────────────┘ └─────────────┘ └────┘
typ └────────────┘ └─────────────┘ ┴ └┘ └┘ └────┘
doc └─────────────┘
74
75 @[ext] theorem ext {f f' : multilinear_map R M₁ M₂} (H : ∀ x, f x = f' x) : f = f' :=
id └─────────────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
doc └─┘ └─────────────┘
76 by cases f; cases f'; congr'; exact funext H
id ┴ └┘ └────┘ ┴
src └────┘ └────┘ └────┘ └────┘└────┘┴ └
typ └────┘┴ └────┘└┘ └────┘ └────┘└────┘┴┴└
doc └────┘ └────┘ └────┘ └────┘ ┴ └
txt └────┘ └────┘ └────┘ └────┘ ┴ └
par └────┘ └────┘ └────┘ └────┘ ┴ └
pid ┴ ┴ ┴ ┴ └
st └──────────────────────────────────────────
77
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
78 @[simp] lemma map_add (m : Πi, M₁ i) (i : ι) (x y : M₁ i) :
id ┴ └┘ ┴ ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴
doc └──┘
79 f (update m i (x + y)) = f (update m i x) + f (update m i y) :=
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘ ┴ ┴ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └────┘ └────┘ └────┘
80 f.add m i x y
id ┴└──┘ ┴ ┴ ┴ ┴
src └──┘
typ ┴└──┘ ┴ ┴ ┴ ┴
81
82 @[simp] lemma map_smul (m : Πi, M₁ i) (i : ι) (c : R) (x : M₁ i) :
id ┴ └┘ ┴ ┴ ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴
doc └──┘
83 f (update m i (c • x)) = c • f (update m i x) :=
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └────┘ └────┘
84 f.smul m i c x
id ┴└───┘ ┴ ┴ ┴ ┴
src └───┘
typ ┴└───┘ ┴ ┴ ┴ ┴
85
86 @[simp] lemma map_sub (m : Πi, M₁ i) (i : ι) (x y : M₁ i) :
id ┴ └┘ ┴ ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴
doc └──┘
87 f (update m i (x - y)) = f (update m i x) - f (update m i y) :=
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘ ┴ ┴ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └────┘ └────┘ └────┘
88 by { simp only [map_add, add_left_inj, sub_eq_add_neg, (neg_one_smul R y).symm, map_smul], simp }
id └─────┘ └──────────┘ └────────────┘ └──────────┘ ┴ ┴ └──────┘
src └─────────┘└─────┘└┘└──────────┘└┘└────────────┘└┘ └──────────┘┴ ┴ └──────┘└──────┘┴ └───┘
typ └─────────┘└─────┘└┘└──────────┘└┘└────────────┘└┘ └──────────┘┴┴┴┴└──────┘└──────┘┴ └───┘
doc └─────────┘ └┘ └┘ └┘ ┴ ┴ └──────┘ ┴ └───┘
txt └─────────┘ └┘ └┘ └┘ ┴ ┴ └──────┘ ┴ └───┘
par └─────────┘ └┘ └┘ └┘ ┴ ┴ └──────┘ ┴ └───┘
pid ┴└──┘└┘ └┘ └┘ └┘ ┴ ┴ └──────┘ ┴ ┴
st └─────────────────────────────────────────────────────────────────────────────────────┘└─────┘└┘
89
90 lemma map_coord_zero {m : Πi, M₁ i} (i : ι) (h : m i = 0) : f m = 0 :=
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
91 begin
st └─────
92 have : (0 : R) • (0 : M₁ i) = 0, by simp,
id ┴ ┴ └┘ ┴ ┴
src └─────┘ └──┘ └┘┴┴ └──┘ ┴ └┘┴└┘ └──┘
typ └─────┘ └──┘┴└┘┴┴ └──┘└┘┴┴└┘┴└┘ └──┘
doc └─────┘ └──┘ └┘ ┴ └──┘ ┴ └┘ └┘ └──┘
txt └─────┘ └──┘ └┘ ┴ └──┘ ┴ └┘ └┘ └──┘
par └─────┘ └──┘ └┘ ┴ └──┘ ┴ └┘ └┘ └──┘
pid └───┘└┘ └──┘ └┘ ┴ └──┘ ┴ └┘ ┴┴
st ────────────────────────────────┘ └─
93 rw [← update_eq_self i m, h, ← this, f.map_smul, zero_smul]
id └────────────┘ ┴ ┴ ┴ └──┘ └───────┘
src └────┘└────────────┘┴ ┴ └┘ └──┘ └┘ └┘└───────┘└┘
typ └────┘└────────────┘┴┴┴┴└┘┴└──┘└──┘└┘└────────┘└┘└───────┘└┘
doc └────┘ ┴ ┴ └┘ └──┘ └┘ └┘ └┘
txt └────┘ ┴ ┴ └┘ └──┘ └┘ └┘ └┘
par └────┘ ┴ ┴ └┘ └──┘ └┘ └┘ └┘
pid └──┘ ┴ ┴ └┘ └──┘ └┘ └┘ ┴┴
st ─────────────────────────┘└─┘└──────┘└──────────┘└─────────┘┴┴
94 end
st └─┘
95
96 @[simp] lemma map_zero [nonempty ι] : f 0 = 0 :=
id └──────┘ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴
doc └──┘
97 begin
st └─────
98 obtain ⟨i, _⟩ : ∃i:ι, i ∈ set.univ := set.exists_mem_of_nonempty ι,
id ┴ ┴ ┴ └──────┘ └────────────────────────┘ ┴
src └──────────────┘┴└┘ ┴┴ ┴┴┴└──────┘└──┘└────────────────────────┘┴
typ └──────────────┘┴└┘ ┴┴ ┴┴┴└──────┘└──┘└────────────────────────┘┴┴
doc └──────────────┘ └┘ ┴ ┴ ┴ └──┘ ┴
txt └──────────────┘ └┘ ┴ ┴ ┴ └──┘ ┴
par └──────────────┘ └┘ ┴ ┴ ┴ └──┘ ┴
pid └────────┘ └┘ ┴ ┴ ┴ └──┘ ┴
st ───────────────────────────────────────────────────────────────────┘└─
99 exact map_coord_zero f i rfl
id └────────────┘ ┴ ┴ └─┘
src └────┘└────────────┘┴ ┴ ┴└─┘┴
typ └────┘└────────────┘┴┴┴┴┴└─┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────┘
100 end
st └─┘
101
102 instance : has_add (multilinear_map R M₁ M₂) :=
id └─────┘ └─────────────┘ ┴ └┘ └┘
src └─────┘ └─────────────┘
typ └─────┘ └─────────────┘ ┴ └┘ └┘
doc └─────────────┘
103 ⟨λf f', ⟨λx, f x + f' x, λm i x y, by simp, λm i c x, by simp [smul_add]⟩⟩
id ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
src ┴ └──┘ └────┘└──────┘┴
typ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └────┘└──────┘┴
doc └──┘ └────┘ ┴
txt └──┘ └────┘ ┴
par └──┘ └────┘ ┴
pid ┴┴ ┴
st └───┘ └──────────────┘
104
105 @[simp] lemma add_apply (m : Πi, M₁ i) : (f + f') m = f m + f' m := rfl
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
doc └──┘
106
107 instance : has_neg (multilinear_map R M₁ M₂) :=
id └─────┘ └─────────────┘ ┴ └┘ └┘
src └─────┘ └─────────────┘
typ └─────┘ └─────────────┘ ┴ └┘ └┘
doc └─────────────┘
108 ⟨λ f, ⟨λ m, - f m, λm i x y, by simp, λm i c x, by simp⟩⟩
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st └───┘ └───┘
109
110 @[simp] lemma neg_apply (m : Πi, M₁ i) : (-f) m = - (f m) := rfl
id ┴ └┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ ┴ └┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
111
112 instance : has_zero (multilinear_map R M₁ M₂) :=
id └──────┘ └─────────────┘ ┴ └┘ └┘
src └──────┘ └─────────────┘
typ └──────┘ └─────────────┘ ┴ └┘ └┘
doc └─────────────┘
113 ⟨⟨λ _, 0, λm i x y, by simp, λm i c x, by simp⟩⟩
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st └───┘ └───┘
114
115 instance : inhabited (multilinear_map R M₁ M₂) := ⟨0⟩
id └───────┘ └─────────────┘ ┴ └┘ └┘
src └───────┘ └─────────────┘
typ └───────┘ └─────────────┘ ┴ └┘ └┘
doc └─────────────┘
116
117 @[simp] lemma zero_apply (m : Πi, M₁ i) : (0 : multilinear_map R M₁ M₂) m = 0 := rfl
id ┴ └┘ ┴ └─────────────┘ ┴ └┘ └┘ ┴ ┴ └─┘
src └─────────────┘ ┴ └─┘
typ ┴ └┘ ┴ └─────────────┘ ┴ └┘ └┘ ┴ ┴ └─┘
doc └──┘ └─────────────┘
118
119 instance : add_comm_group (multilinear_map R M₁ M₂) :=
id └────────────┘ └─────────────┘ ┴ └┘ └┘
src └────────────┘ └─────────────┘
typ └────────────┘ └─────────────┘ ┴ └┘ └┘
doc └─────────────┘
120 by refine {zero := 0, add := (+), neg := has_neg.neg, ..};
id ┴ └─────────┘
src └─────┘ └────────────────┘┴└─────────┘└─────────┘└───┘
typ └─────┘ └────────────────┘┴└─────────┘└─────────┘└───┘
doc └─────┘ └────────────────┘ └─────────┘ └───┘
txt └─────┘ └────────────────┘ └─────────┘ └───┘
par └─────┘ └────────────────┘ └─────────┘ └───┘
pid ┴ └────────────────┘ └─────────┘ └───┘
st └────────────────────────────────────────────────────────
121 intros; ext; simp
src └────┘ └─┘ └────
typ └────┘ └─┘ └────
doc └────┘ └─┘ └────
txt └────┘ └─┘ └────
par └────┘ └─┘ └────
pid └
st ─────────────────────
122
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
123 /-- If `f` is a multilinear map, then `f.to_linear_map m i` is the linear map obtained by fixing all
124 coordinates but `i` equal to those of `m`, and varying the `i`-th coordinate. -/
125 def to_linear_map (m : Πi, M₁ i) (i : ι) : M₁ i →ₗ[R] M₂ :=
id ┴ └┘ ┴ ┴ └┘ ┴ └─┘┴┴ └┘
src └─┘ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ └─┘┴┴ └┘
126 { to_fun := λx, f (update m i x),
id ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘
typ ┴ ┴ └────┘ ┴ ┴ ┴
doc └────┘
127 add := λx y, by simp,
id ┴ ┴
src └──┘
typ ┴ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
128 smul := λc x, by simp }
id ┴ ┴
src └───┘
typ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
129
130 /-- In the specific case of multilinear maps on spaces indexed by `fin (n+1)`, where one can build
131 an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the additivity of a
132 multilinear map along the first variable. -/
133 lemma cons_add (f : multilinear_map R M M₂) (m : Π(i : fin n), M i.succ) (x y : M 0) :
id └─────────────┘ ┴ ┴ └┘ └─┘ ┴ ┴ ┴└───┘ ┴
src └─────────────┘ └─┘ └───┘
typ └─────────────┘ ┴ ┴ └┘ └─┘ ┴ ┴ ┴└───┘ ┴
doc └─────────────┘
134 f (cons (x+y) m) = f (cons x m) + f (cons y m) :=
id ┴ └──┘ ┴┴┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ ┴ ┴ └──┘ ┴ └──┘
typ ┴ └──┘ ┴┴┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘ └──┘ └──┘
135 by rw [← update_cons_zero x m (x+y), f.map_add, update_cons_zero, update_cons_zero]
id └──────────────┘ ┴ ┴┴┴ └──────────────┘ └──────────────┘
src └────┘└──────────────┘┴ ┴ ┴ ┴ └─┘ └┘└──────────────┘└┘└──────────────┘└─
typ └────┘└──────────────┘┴ ┴┴┴ ┴┴┴└─┘└───────┘└┘└──────────────┘└┘└──────────────┘└─
doc └────┘└──────────────┘┴ ┴ ┴ └─┘ └┘└──────────────┘└┘└──────────────┘└─
txt └────┘ ┴ ┴ ┴ └─┘ └┘ └┘ └─
par └────┘ ┴ ┴ ┴ └─┘ └┘ └┘ └─
pid └──┘ ┴ ┴ ┴ └─┘ └┘ └┘ ┴└
st └───────────────────────────────┘└─────────┘└────────────────┘└────────────────┘┴└
136
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
137 /-- In the specific case of multilinear maps on spaces indexed by `fin (n+1)`, where one can build
138 an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the multiplicativity
139 of a multilinear map along the first variable. -/
140 lemma cons_smul (f : multilinear_map R M M₂) (m : Π(i : fin n), M i.succ) (c : R) (x : M 0) :
id └─────────────┘ ┴ ┴ └┘ └─┘ ┴ ┴ ┴└───┘ ┴ ┴
src └─────────────┘ └─┘ └───┘
typ └─────────────┘ ┴ ┴ └┘ └─┘ ┴ ┴ ┴└───┘ ┴ ┴
doc └─────────────┘
141 f (cons (c • x) m) = c • f (cons x m) :=
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ ┴ ┴ ┴ └──┘
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘ └──┘
142 by rw [← update_cons_zero x m (c • x), f.map_smul, update_cons_zero]
id └──────────────┘ ┴ ┴ ┴ ┴ └──────────────┘
src └────┘└──────────────┘┴ ┴ ┴ ┴┴┴ └─┘ └┘└──────────────┘└─
typ └────┘└──────────────┘┴ ┴┴┴ ┴┴┴┴┴└─┘└────────┘└┘└──────────────┘└─
doc └────┘└──────────────┘┴ ┴ ┴ ┴ ┴ └─┘ └┘└──────────────┘└─
txt └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ └─
par └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ └─
pid └──┘ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ ┴└
st └─────────────────────────────────┘└──────────┘└────────────────┘┴└
143
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
144 end ring
145
146 section comm_ring
147
148 variables [comm_ring R] [∀i, add_comm_group (M₁ i)] [∀i, add_comm_group (M i)] [add_comm_group M₂]
id └───────┘ ┴ └────────────┘ ┴ ┴ └────────────┘ ┴ └────────────┘
src └───────┘ └────────────┘ └────────────┘ └────────────┘
typ └───────┘ ┴ └────────────┘ ┴ ┴ └────────────┘ ┴ └────────────┘
149 [∀i, module R (M i)] [∀i, module R (M₁ i)] [module R M₂]
id ┴ └────┘ ┴ ┴ └────┘ ┴ └────┘
src └────┘ └────┘ └────┘
typ ┴ └────┘ ┴ ┴ └────┘ ┴ └────┘
doc └────┘ └────┘ └────┘
150 (f f' : multilinear_map R M₁ M₂)
id └─────────────┘
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
151
152 /-- If one multiplies by `c i` the coordinates in a finset `s`, then the image under a multilinear
153 map is multiplied by `s.prod c`. This is mainly an auxiliary statement to prove the result when
154 `s = univ`, given in `map_smul_univ`, although it can be useful in its own right as it does not
155 require the index set `ι` to be finite. -/
156 lemma map_piecewise_smul (c : ι → R) (m : Πi, M₁ i) (s : finset ι) :
id ┴ ┴ ┴ └┘ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ └┘ ┴ └────┘ ┴
doc └────┘
157 f (s.piecewise (λi, c i • m i) m) = s.prod c • f m :=
id ┴ ┴└────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ └───┘ ┴
typ ┴ ┴└────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴
doc └────────┘ └───┘
158 begin
st └─────
159 refine s.induction_on (by simp) _,
id └────────────┘
src └─────┘└────────────┘┴ ┴└──┘└─┘
typ └─────┘└────────────┘┴ ┴└──┘└─┘
doc └─────┘└────────────┘┴ ┴└──┘└─┘
txt └─────┘ ┴ ┴└──┘└─┘
par └─────┘ ┴ ┴└──┘└─┘
pid ┴ ┴ └──────┘
st ──────────────────────────┘└───┘└─┘└─
160 assume j s j_not_mem_s Hrec,
src └─────────────────────────┘
typ └─────────────────────────┘
doc └─────────────────────────┘
txt └─────────────────────────┘
par └─────────────────────────┘
pid └─────────────────────────┘
st ────────────────────────────┘└─
161 have A : function.update (s.piecewise (λi, c i • m i) m) j (m j) =
id └─────────────┘ ┴ ┴ ┴
src └───────┘└─────────────┘┴ ┴ └─┘ ┴ ┴┴┴ ┴ └┘ └┘ ┴ ┴ └┘┴└
typ └───────┘└─────────────┘┴ ┴ └─┘ ┴ ┴┴┴ ┴ └┘ └┘ ┴ ┴┴└┘┴└
doc └───────┘└─────────────┘┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └
txt └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └
par └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └
pid └────┘└─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └
st ─────────────────────────────────────────────────────────────────────
162 s.piecewise (λi, c i • m i) m,
id └─────────┘ ┴ ┴
src ──────────┘└─────────┘┴ └─┘ ┴ ┴ ┴ ┴ └┘
typ ──────────┘└─────────┘┴ └─┘┴┴ ┴ ┴ ┴ └┘┴
doc ──────────┘└─────────┘┴ └─┘ ┴ ┴ ┴ ┴ └┘
txt ──────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
par ──────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
pid ──────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────┘└─
163 { ext i,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ───┘└───┘└─
164 by_cases h : i = j,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ─────────────────────┘└─
165 { rw h, simp [j_not_mem_s] },
id ┴ └─────────┘
src └─┘ └────┘ └┘
typ └─┘┴ └────┘└─────────┘└┘
doc └─┘ └────┘ └┘
txt └─┘ └────┘ └┘
par └─┘ └────┘ └┘
pid ┴ ┴┴ ┴┴
st ─────┘└──┘└───────────────────┘└┘└
166 { simp [h] } },
id ┴
src └────┘ └┘
typ └────┘┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ──────────────┘└──┘└
167 rw [s.piecewise_insert, f.map_smul, A, Hrec],
id ┴ └──┘
src └──┘ └┘ └┘ └┘ ┴
typ └──┘└────────────────┘└┘└────────┘└┘┴└┘└──┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ───────────────────────┘└──────────┘└─┘└────┘└──
168 simp [j_not_mem_s, mul_smul]
id └─────────┘ └──────┘
src └────┘ └┘└──────┘└┘
typ └────┘└─────────┘└┘└──────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ──────────────────────────────┘
169 end
st └─┘
170
171 /-- Multiplicativity of a multilinear map along all coordinates at the same time,
172 writing `f (λi, c i • m i)` as `univ.prod c • f m`. -/
173 lemma map_smul_univ [fintype ι] (c : ι → R) (m : Πi, M₁ i) :
id └─────┘ ┴ ┴ ┴ ┴ └┘ ┴
src └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ └┘ ┴
doc └─────┘
174 f (λi, c i • m i) = finset.univ.prod c • f m :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴ ┴
src ┴ ┴ └─────────┘└───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴ ┴
doc └─────────┘└───┘
175 by simpa using map_piecewise_smul f c m finset.univ
id └────────────────┘ ┴ ┴ ┴ └─────────┘
src └──────────┘└────────────────┘┴ ┴ ┴ ┴└─────────┘└
typ └──────────┘└────────────────┘┴┴┴┴┴┴┴└─────────┘└
doc └──────────┘└────────────────┘┴ ┴ ┴ ┴└─────────┘└
txt └──────────┘ ┴ ┴ ┴ ┴ └
par └──────────┘ ┴ ┴ ┴ ┴ └
pid ┴└────┘ ┴ ┴ ┴ ┴ └
st └─────────────────────────────────────────────────
176
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
177 /-- If one adds to a vector `m'` another vector `m`, but only for coordinates in a finset `t`, then
178 the image under a multilinear map `f` is the sum of `f (s.piecewise m m')` along all subsets `s` of
179 `t`. This is mainly an auxiliary statement to prove the result when `t = univ`, given in
180 `map_add_univ`, although it can be useful in its own right as it does not require the index set `ι`
181 to be finite.-/
182 lemma map_piecewise_add (m m' : Πi, M₁ i) (t : finset ι) :
id ┴ └┘ ┴ └────┘ ┴
src └────┘
typ ┴ └┘ ┴ └────┘ ┴
doc └────┘
183 f (t.piecewise (m + m') m') = t.powerset.sum (λs, f (s.piecewise m m')) :=
id ┴ ┴└────────┘ ┴ ┴ └┘ └┘ ┴ ┴└───────┘└──┘ ┴ ┴ ┴└────────┘ ┴ └┘
src └────────┘ ┴ ┴ └───────┘└──┘ └────────┘
typ ┴ ┴└────────┘ ┴ ┴ └┘ └┘ ┴ ┴└───────┘└──┘ ┴ ┴ ┴└────────┘ ┴ └┘
doc └────────┘ └───────┘ └────────┘
184 begin
st └─────
185 revert m',
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └─┘
st ──────────┘└─
186 refine finset.induction_on t (by simp) _,
id └─────────────────┘ ┴
src └─────┘└─────────────────┘┴ ┴ ┴└──┘└─┘
typ └─────┘└─────────────────┘┴┴┴ ┴└──┘└─┘
doc └─────┘└─────────────────┘┴ ┴ ┴└──┘└─┘
txt └─────┘ ┴ ┴ ┴└──┘└─┘
par └─────┘ ┴ ┴ ┴└──┘└─┘
pid ┴ ┴ ┴ └──────┘
st ─────────────────────────────────┘└───┘└─┘└─
187 assume i t hit Hrec m',
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └────────────────────┘
st ───────────────────────┘└─
188 have A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i) :=
id └────┘ ┴ ┴ └────┘ └─────────┘ ┴ └┘ ┴
src └───────┘ └────┘┴ ┴ └──────────┘ ┴┴┴ └┘ ┴┴┴└────┘┴ └─────────┘┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └────
typ └───────┘ └────┘┴ ┴ └──────────┘ ┴┴┴ └┘ ┴┴┴└────┘┴ └─────────┘┴ ┴ ┴ └┘ └┘ ┴ ┴┴ ┴ ┴└┘┴┴└────
doc └───────┘ ┴ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴└────┘┴ └─────────┘┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └────
txt └───────┘ ┴ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └────
par └───────┘ ┴ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └────
pid └────┘└─┘ ┴ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴└───
st ───────────────────────────────────────────────────────────────────────────────────────────────────
189 t.piecewise_insert _ _ _,
id └────────────────┘
src ───┘└────────────────┘└────┘
typ ───┘└────────────────┘└────┘
doc ───┘ └────┘
txt ───┘ └────┘
par ───┘ └────┘
pid ───┘ └────┘
st ───────────────────────────┘└─
190 have B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m',
id └────┘ ┴ └─────────┘ ┴ └┘
src └───────┘└────┘┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴└─────────┘┴ ┴ ┴ └┘
typ └───────┘└────┘┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴┴└┘ ┴└─────────┘┴ ┴┴ ┴ └┘└┘
doc └───────┘└────┘┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴└─────────┘┴ ┴ ┴ └┘
txt └───────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └───────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └────┘└─┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────────┘└─
191 { ext j,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ───┘└───┘└─
192 by_cases h : j = i,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ─────────────────────┘└─
193 { rw h, simp [hit] },
id ┴ └─┘
src └─┘ └────┘ └┘
typ └─┘┴ └────┘└─┘└┘
doc └─┘ └────┘ └┘
txt └─┘ └────┘ └┘
par └─┘ └────┘ └┘
pid ┴ ┴┴ ┴┴
st ─────┘└──┘└───────────┘└┘└
194 { simp [h] } },
id ┴
src └────┘ └┘
typ └────┘┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ──────────────┘└──┘└
195 let m'' := update m' i (m i),
id └────┘ └┘ ┴ ┴
src └─────────┘└────┘┴ ┴ ┴ ┴ ┴
typ └─────────┘└────┘┴└┘┴ ┴ ┴┴┴┴
doc └─────────┘└────┘┴ ┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────┘└─
196 have C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m'',
id └────┘ └┘ ┴ └─────────┘ ┴ └─┘
src └───────┘└────┘┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴└─────────┘┴ ┴ ┴ └┘
typ └───────┘└────┘┴ ┴ ┴ ┴ └┘└┘└┘ ┴ ┴┴└┘ ┴└─────────┘┴ ┴┴ ┴ └┘└─┘
doc └───────┘└────┘┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴└─────────┘┴ ┴ ┴ └┘
txt └───────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └───────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └────┘└─┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────┘└─
197 { ext j,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ───┘└───┘└─
198 by_cases h : j = i,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ─────────────────────┘└─
199 { rw h, simp [m'', hit] },
id ┴ └─┘ └─┘
src └─┘ └────┘ └┘ └┘
typ └─┘┴ └────┘└─┘└┘└─┘└┘
doc └─┘ └────┘ └┘ └┘
txt └─┘ └────┘ └┘ └┘
par └─┘ └────┘ └┘ └┘
pid ┴ ┴┴ └┘ ┴┴
st ─────┘└──┘└────────────────┘└┘└
200 { by_cases h' : j ∈ t; simp [h, hit, m'', h'] } },
id ┴ ┴ ┴ ┴ └─┘ └─┘ └┘
src └───────┘ └─┘ ┴┴┴ └────┘ └┘ └┘ └┘ └┘
typ └───────┘ └─┘┴┴┴┴┴ └────┘┴└┘└─┘└┘└─┘└┘└┘└┘
doc └───────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └┘ └┘
txt └───────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └┘ └┘
par └───────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └┘ └┘
pid ┴ └─┘ ┴ ┴ ┴┴ └┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────────────┘└──┘└
201 rw [A, f.map_add, B, C, finset.sum_powerset_insert hit, Hrec, Hrec, add_comm],
id ┴ ┴ ┴ └────────────────────────┘ └─┘ └──┘ └──┘ └──────┘
src └──┘ └┘ └┘ └┘ └┘└────────────────────────┘┴ └┘ └┘ └┘└──────┘┴
typ └──┘┴└┘└───────┘└┘┴└┘┴└┘└────────────────────────┘┴└─┘└┘└──┘└┘└──┘└┘└──────┘┴
doc └──┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴
st ──────┘└─────────┘└─┘└─┘└──────────────────────────────┘└────┘└────┘└────────┘└──
202 congr' 1,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴┴
st ─────────┘└─
203 apply finset.sum_congr rfl (λs hs, _),
id └──────────────┘ └─┘
src └────┘└──────────────┘┴└─┘┴ └──────┘
typ └────┘└──────────────┘┴└─┘┴ └──────┘
doc └────┘ ┴ ┴ └──────┘
txt └────┘ ┴ ┴ └──────┘
par └────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ └──────┘
st ──────────────────────────────────────┘└─
204 have : (insert i s).piecewise m m' = s.piecewise m m'',
id └────┘ ┴ └┘ └─────────┘ ┴ └─┘
src └─────┘ └────┘┴ ┴ └──────────┘ ┴ ┴ ┴└─────────┘┴ ┴
typ └─────┘ └────┘┴┴┴ └──────────┘ ┴└┘┴ ┴└─────────┘┴┴┴└─┘
doc └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴└─────────┘┴ ┴
txt └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
205 { ext j,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ───┘└───┘└─
206 by_cases h : j = i,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ─────────────────────┘└─
207 { rw h, simp [m'', finset.not_mem_of_mem_powerset_of_not_mem hs hit] },
id ┴ └─┘ └───────────────────────────────────────┘ └┘ └─┘
src └─┘ └────┘ └┘└───────────────────────────────────────┘┴ ┴ └┘
typ └─┘┴ └────┘└─┘└┘└───────────────────────────────────────┘┴└┘┴└─┘└┘
doc └─┘ └────┘ └┘ ┴ ┴ └┘
txt └─┘ └────┘ └┘ ┴ ┴ └┘
par └─┘ └────┘ └┘ ┴ ┴ └┘
pid ┴ ┴┴ └┘ ┴ ┴ ┴┴
st ─────┘└──┘└─────────────────────────────────────────────────────────────┘└┘└
208 { by_cases h' : j ∈ s; simp [h, m'', h'] } },
id ┴ ┴ ┴ └─┘ └┘
src └───────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └┘
typ └───────┘ └─┘┴┴ ┴┴ └────┘┴└┘└─┘└┘└┘└┘
doc └───────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └┘
txt └───────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └┘
par └───────┘ └─┘ ┴ ┴ └────┘ └┘ └┘ └┘
pid ┴ └─┘ ┴ ┴ ┴┴ └┘ └┘ ┴┴
st ────────────────────────────────────────────┘└──┘└
209 rw this
id └──┘
src └─┘ ┴
typ └─┘└──┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ─────────┘
210 end
st └─┘
211
212 /-- Additivity of a multilinear map along all coordinates at the same time,
213 writing `f (m + m')` as the sum of `f (s.piecewise m m')` over all sets `s`. -/
214 lemma map_add_univ [fintype ι] (m m' : Πi, M₁ i) :
id └─────┘ ┴ ┴ └┘ ┴
src └─────┘
typ └─────┘ ┴ ┴ └┘ ┴
doc └─────┘
215 f (m + m') = (finset.univ : finset (finset ι)).sum (λs, f (s.piecewise m m')) :=
id ┴ ┴ ┴ └┘ ┴ └─────────┘ └────┘ └────┘ ┴ └─┘ ┴ ┴ ┴└────────┘ ┴ └┘
src ┴ ┴ └─────────┘ └────┘ └────┘ └─┘ └────────┘
typ ┴ ┴ ┴ └┘ ┴ └─────────┘ └────┘ └────┘ ┴ └─┘ ┴ ┴ ┴└────────┘ ┴ └┘
doc └─────────┘ └────┘ └────┘ └────────┘
216 by simpa using f.map_piecewise_add m m' finset.univ
id └─────────────────┘ ┴ └┘ └─────────┘
src └──────────┘└─────────────────┘┴ ┴ ┴└─────────┘└
typ └──────────┘└─────────────────┘┴┴┴└┘┴└─────────┘└
doc └──────────┘└─────────────────┘┴ ┴ ┴└─────────┘└
txt └──────────┘ ┴ ┴ ┴ └
par └──────────┘ ┴ ┴ ┴ └
pid ┴└────┘ ┴ ┴ ┴ └
st └─────────────────────────────────────────────────
217
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
218 instance : has_scalar R (multilinear_map R M₁ M₂) := ⟨λ c f,
id └────────┘ ┴ └─────────────┘ ┴ └┘ └┘ ┴ ┴
src └────────┘ └─────────────┘
typ └────────┘ ┴ └─────────────┘ ┴ └┘ └┘ ┴ ┴
doc └────────┘ └─────────────┘
219 ⟨λ m, c • f m, λm i x y, by simp [smul_add], λl i x d, by simp [smul_smul, mul_comm]⟩⟩
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └───────┘ └──────┘
src ┴ └────┘└──────┘┴ └────┘└───────┘└┘└──────┘┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────┘┴ ┴ ┴ ┴ ┴ └────┘└───────┘└┘└──────┘┴
doc └────┘ ┴ └────┘ └┘ ┴
txt └────┘ ┴ └────┘ └┘ ┴
par └────┘ ┴ └────┘ └┘ ┴
pid ┴┴ ┴ ┴┴ └┘ ┴
st └──────────────┘ └─────────────────────────┘
220
221 @[simp] lemma smul_apply (c : R) (m : Πi, M₁ i) : (c • f) m = c • f m := rfl
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
222
223 /-- The space of multilinear maps is a module over `R`, for the pointwise addition and scalar
224 multiplication. -/
225 instance : module R (multilinear_map R M₁ M₂) :=
id └────┘ ┴ └─────────────┘ ┴ └┘ └┘
src └────┘ └─────────────┘
typ └────┘ ┴ └─────────────┘ ┴ └┘ └┘
doc └────┘ └─────────────┘
226 module.of_core $ by refine { smul := (•), ..};
id └────────────┘ ┴
src └────────────┘ └─────┘ └───────┘┴└─────┘
typ └────────────┘ └─────┘ └───────┘┴└─────┘
doc └─────┘ └───────┘ └─────┘
txt └─────┘ └───────┘ └─────┘
par └─────┘ └───────┘ └─────┘
pid ┴ └───────┘ └─────┘
st └───────────────────────────
227 intros; ext; simp [smul_add, add_smul, smul_smul]
id └──────┘ └──────┘ └───────┘
src └────┘ └─┘ └────┘└──────┘└┘└──────┘└┘└───────┘└─
typ └────┘ └─┘ └────┘└──────┘└┘└──────┘└┘└───────┘└─
doc └────┘ └─┘ └────┘ └┘ └┘ └─
txt └────┘ └─┘ └────┘ └┘ └┘ └─
par └────┘ └─┘ └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st ────────────────────────────────────────────────────
228
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
229 variables (R ι)
230
231 /-- The canonical multilinear map on `R^ι` when `ι` is finite, associating to `m` the product of
232 all the `m i` (multiplied by a fixed reference element `z` in the target module) -/
233 protected def mk_pi_ring [fintype ι] (z : M₂) : multilinear_map R (λ(i : ι), R) M₂ :=
id └─────┘ ┴ └┘ └─────────────┘ ┴ ┴ ┴ └┘
src └─────┘ └─────────────┘
typ └─────┘ ┴ └┘ └─────────────┘ ┴ ┴ ┴ └┘
doc └─────┘ └─────────────┘
234 { to_fun := λm, finset.univ.prod m • z,
id ┴ └─────────┘└───┘ ┴ ┴ ┴
src └─────────┘└───┘ ┴
typ ┴ └─────────┘└───┘ ┴ ┴ ┴
doc └─────────┘└───┘
235 add := λ m i x y, by simp [finset.prod_update_of_mem, add_mul, add_smul],
id ┴ ┴ ┴ ┴ └───────────────────────┘ └─────┘ └──────┘
src └────┘└───────────────────────┘└┘└─────┘└┘└──────┘┴
typ ┴ ┴ ┴ ┴ └────┘└───────────────────────┘└┘└─────┘└┘└──────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └──────────────────────────────────────────────────┘
236 smul := λ m i c x, by { rw [smul_eq_mul], simp [finset.prod_update_of_mem, smul_smul, mul_assoc] } }
id ┴ ┴ ┴ ┴ └─────────┘ └───────────────────────┘ └───────┘ └───────┘
src └──┘└─────────┘┴ └────┘└───────────────────────┘└┘└───────┘└┘└───────┘└┘
typ ┴ ┴ ┴ ┴ └──┘└─────────┘┴ └────┘└───────────────────────┘└┘└───────┘└┘└───────┘└┘
doc └──┘ ┴ └────┘ └┘ └┘ └┘
txt └──┘ ┴ └────┘ └┘ └┘ └┘
par └──┘ ┴ └────┘ └┘ └┘ └┘
pid └┘ ┴ ┴┴ └┘ └┘ ┴┴
st └────────────────┘└────────────────────────────────────────────────────────┘└┘
237
238 variables {R ι}
239
240 @[simp] lemma mk_pi_ring_apply [fintype ι] (z : M₂) (m : ι → R) :
id └─────┘ ┴ └┘ ┴ ┴
src └─────┘
typ └─────┘ ┴ └┘ ┴ ┴
doc └──┘ └─────┘
241 (multilinear_map.mk_pi_ring R ι z : (ι → R) → M₂) m = finset.univ.prod m • z := rfl
id └────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴ └─┘
src └────────────────────────┘ ┴ └─────────┘└───┘ ┴ └─┘
typ └────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─────────┘└───┘ ┴ ┴ ┴ └─┘
doc └────────────────────────┘ └─────────┘└───┘
242
243 lemma mk_pi_ring_apply_one_eq_self [fintype ι] (f : multilinear_map R (λ(i : ι), R) M₂) :
id └─────┘ ┴ └─────────────┘ ┴ ┴ ┴ └┘
src └─────┘ └─────────────┘
typ └─────┘ ┴ └─────────────┘ ┴ ┴ ┴ └┘
doc └─────┘ └─────────────┘
244 multilinear_map.mk_pi_ring R ι (f (λi, 1)) = f :=
id └────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────────────┘ ┴
typ └────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────────────┘
245 begin
st └─────
246 ext m,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
247 have : m = (λi, m i • 1), by { ext j, simp },
id ┴ ┴ ┴
src └─────┘ ┴┴┴ └─┘ ┴ ┴┴└─┘ └───┘ └───┘
typ └─────┘ ┴┴┴ └─┘┴┴ ┴┴└─┘ └───┘ └───┘
doc └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ └───┘ └───┘
txt └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ └───┘ └───┘
par └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ └───┘ └───┘
pid └───┘└┘ ┴ ┴ └─┘ ┴ ┴ └─┘ └┘ ┴
st ─────────────────────────┘ ┴└────┘└─────┘└┘└
248 conv_rhs { rw [this, f.map_smul_univ] },
id └──┘
src └─────────┘└──┘ └┘ └┘┴
typ └─────────┘└──┘└──┘└┘└─────────────┘└┘┴
txt └─────────┘└──┘ └┘ └┘┴
par └─────────┘└──┘ └┘ └┘┴
pid ┴└────┘ └┘ └─┘
st ───────────┘└───────┘└───────────────┘ ┴└┘└
249 refl
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
250 end
st └─┘
251
252 variables (R ι M₂)
253 /-- When `ι` is finite, multilinear maps on `R^ι` with values in `M₂` are in bijection with `M₂`,
254 as such a multilinear map is completely determined by its value on the constant vector made of ones.
255 We register this bijection as a linear equivalence in `multilinear_map.pi_ring_equiv`. -/
256 protected def pi_ring_equiv [fintype ι] : M₂ ≃ₗ[R] (multilinear_map R (λ(i : ι), R) M₂) :=
id └─────┘ ┴ └┘ └─┘┴┴ └─────────────┘ ┴ ┴ ┴ └┘
src └─────┘ └─┘ ┴ └─────────────┘
typ └─────┘ ┴ └┘ └─┘┴┴ └─────────────┘ ┴ ┴ ┴ └┘
doc └─────┘ └─┘ ┴ └─────────────┘
257 { to_fun := λ z, multilinear_map.mk_pi_ring R ι z,
id ┴ └────────────────────────┘ ┴ ┴ ┴
src └────────────────────────┘
typ ┴ └────────────────────────┘ ┴ ┴ ┴
doc └────────────────────────┘
258 inv_fun := λ f, f (λi, 1),
id ┴ ┴ ┴
typ ┴ ┴ ┴
259 add := λ z z', by { ext m, simp [smul_add] },
id ┴ └┘ └──────┘
src └───┘ └────┘└──────┘└┘
typ ┴ └┘ └───┘ └────┘└──────┘└┘
doc └───┘ └────┘ └┘
txt └───┘ └────┘ └┘
par └───┘ └────┘ └┘
pid └┘ ┴┴ ┴┴
st └──────┘└────────────────┘└┘
260 smul := λ c z, by { ext m, simp [smul_smul, mul_comm] },
id ┴ ┴ └───────┘ └──────┘
src └───┘ └────┘└───────┘└┘└──────┘└┘
typ ┴ ┴ └───┘ └────┘└───────┘└┘└──────┘└┘
doc └───┘ └────┘ └┘ └┘
txt └───┘ └────┘ └┘ └┘
par └───┘ └────┘ └┘ └┘
pid └┘ ┴┴ └┘ ┴┴
st └──────┘└───────────────────────────┘└┘
261 left_inv := λ z, by simp,
id ┴
src └──┘
typ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
262 right_inv := λ f, f.mk_pi_ring_apply_one_eq_self }
id ┴ ┴└───────────────────────────┘
src └───────────────────────────┘
typ ┴ ┴└───────────────────────────┘
263
264 end comm_ring
265
266 end multilinear_map
267
268 section currying
269 /-!
270 ### Currying
271
272 We associate to a multilinear map in `n+1` variables (i.e., based on `fin n.succ`) two
273 curried functions, named `f.curry_left` (which is a linear map on `E 0` taking values
274 in multilinear maps in `n` variables) and `f.curry_right` (wich is a multilinear map in `n`
275 variables taking values in linear maps on `E 0`). In both constructions, the variable that is
276 singled out is `0`, to take advantage of the operations `cons` and `tail` on `fin n`.
277 The inverse operations are called `uncurry_left` and `uncurry_right`.
278
279 We also register linear equiv versions of these correspondences, in
280 `multilinear_curry_left_equiv` and `multilinear_curry_right_equiv`.
281 -/
282 open multilinear_map
283
284 variables {R M M₂}
285 [comm_ring R] [∀i, add_comm_group (M i)] [add_comm_group M₂]
id └───────┘ ┴ └────────────┘ ┴ └────────────┘
src └───────┘ └────────────┘ └────────────┘
typ └───────┘ ┴ └────────────┘ ┴ └────────────┘
286 [∀i, module R (M i)] [module R M₂]
id ┴ └────┘ ┴ └────┘
src └────┘ └────┘
typ ┴ └────┘ ┴ └────┘
doc └────┘ └────┘
287
288 /-- Given a linear map `f` from `M 0` to multilinear maps on `n` variables,
289 construct the corresponding multilinear map on `n+1` variables obtained by concatenating
290 the variables, given by `m ↦ f (m 0) (tail m)`-/
291 def linear_map.uncurry_left
292 (f : M 0 →ₗ[R] (multilinear_map R (λ(i : fin n), M i.succ) M₂)) :
id ┴ └─┘┴┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ └┘
src └─┘ ┴ └─────────────┘ └─┘ └───┘
typ ┴ └─┘┴┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ └┘
doc └─────────────┘
293 multilinear_map R M M₂ :=
id └─────────────┘ ┴ ┴ └┘
src └─────────────┘
typ └─────────────┘ ┴ ┴ └┘
doc └─────────────┘
294 { to_fun := λm, f (m 0) (tail m),
id ┴ ┴ ┴ └──┘ ┴
src └──┘
typ ┴ ┴ ┴ └──┘ ┴
doc └──┘
295 add := λm i x y, begin
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st └─────
296 by_cases h : i = 0,
id ┴ ┴
src └───────┘ └─┘ ┴┴└┘
typ └───────┘ └─┘┴┴┴└┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ─────────────────────┘└─
297 { revert x y,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ─────┘└────────┘└─
298 rw h,
id ┴
src └─┘
typ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────┘└─
299 assume x y,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────────────┘└─
300 rw [update_same, update_same, update_same, f.map_add, add_apply,
id └─────────┘ └─────────┘ └─────────┘ └───────┘
src └──┘└─────────┘└┘└─────────┘└┘└─────────┘└┘ └┘└───────┘└─
typ └──┘└─────────┘└┘└─────────┘└┘└─────────┘└┘└───────┘└┘└───────┘└─
doc └──┘ └┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └┘ └─
st ────────────────────┘└───────────┘└───────────┘└─────────┘└─────────┘└─
301 tail_update_zero, tail_update_zero, tail_update_zero] },
id └──────────────┘ └──────────────┘ └──────────────┘
src ─────────┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘
typ ─────────┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘
doc ─────────┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘
txt ─────────┘ └┘ └┘ └┘
par ─────────┘ └┘ └┘ └┘
pid ─────────┘ └┘ └┘ ┴┴
st ─────────────────────────┘└────────────────┘└────────────────┘┴┴└┘└
302 { rw [update_noteq (ne.symm h), update_noteq (ne.symm h), update_noteq (ne.symm h)],
id └──────────┘ └─────┘ ┴ └──────────┘ └─────┘ ┴ └──────────┘ └─────┘ ┴
src └──┘└──────────┘┴ └─────┘┴ └─┘└──────────┘┴ └─────┘┴ └─┘└──────────┘┴ └─────┘┴ └┘
typ └──┘└──────────┘┴ └─────┘┴┴└─┘└──────────┘┴ └─────┘┴┴└─┘└──────────┘┴ └─────┘┴┴└┘
doc └──┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
txt └──┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
par └──┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
pid └┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
st ─────────────────────────────────┘└────────────────────────┘└────────────────────────┘└──
303 revert x y,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ───────────────┘└─
304 rw ← succ_pred i h,
id └───────┘ ┴ ┴
src └───┘└───────┘┴ ┴
typ └───┘└───────┘┴┴┴┴
doc └───┘ ┴ ┴
txt └───┘ ┴ ┴
par └───┘ ┴ ┴
pid └─┘ ┴ ┴
st ───────────────────────┘└─
305 assume x y,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────────────┘└─
306 rw [tail_update_succ, map_add, tail_update_succ, tail_update_succ] }
id └──────────────┘ └─────┘ └──────────────┘ └──────────────┘
src └──┘└──────────────┘└┘└─────┘└┘└──────────────┘└┘└──────────────┘└┘
typ └──┘└──────────────┘└┘└─────┘└┘└──────────────┘└┘└──────────────┘└┘
doc └──┘└──────────────┘└┘ └┘└──────────────┘└┘└──────────────┘└┘
txt └──┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ ┴┴
st ─────────────────────────┘└───────┘└────────────────┘└────────────────┘┴┴└─
307 end,
st ────┘
308 smul := λm i c x, begin
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st └─────
309 by_cases h : i = 0,
id ┴
src └───────┘ └─┘ ┴ └┘
typ └───────┘ └─┘┴┴ └┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ─────────────────────┘└─
310 { revert x,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────┘└──────┘└─
311 rw h,
id ┴
src └─┘
typ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────┘└─
312 assume x,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────────┘└─
313 rw [update_same, update_same, tail_update_zero, tail_update_zero,
id └─────────┘ └─────────┘ └──────────────┘ └──────────────┘
src └──┘└─────────┘└┘└─────────┘└┘└──────────────┘└┘└──────────────┘└─
typ └──┘└─────────┘└┘└─────────┘└┘└──────────────┘└┘└──────────────┘└─
doc └──┘ └┘ └┘└──────────────┘└┘└──────────────┘└─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └─
st ────────────────────┘└───────────┘└────────────────┘└────────────────┘└─
314 ← smul_apply, f.map_smul] },
id └────────┘
src ───────────┘└────────┘└┘ └┘
typ ───────────┘└────────┘└┘└────────┘└┘
doc ───────────┘ └┘ └┘
txt ───────────┘ └┘ └┘
par ───────────┘ └┘ └┘
pid ───────────┘ └┘ ┴┴
st ─────────────────────┘└──────────┘┴┴└┘└
315 { rw [update_noteq (ne.symm h), update_noteq (ne.symm h)],
id └──────────┘ └─────┘ ┴ └──────────┘ └─────┘ ┴
src └──┘└──────────┘┴ └─────┘┴ └─┘└──────────┘┴ └─────┘┴ └┘
typ └──┘└──────────┘┴ └─────┘┴┴└─┘└──────────┘┴ └─────┘┴┴└┘
doc └──┘ ┴ ┴ └─┘ ┴ ┴ └┘
txt └──┘ ┴ ┴ └─┘ ┴ ┴ └┘
par └──┘ ┴ ┴ └─┘ ┴ ┴ └┘
pid └┘ ┴ ┴ └─┘ ┴ ┴ └┘
st ─────────────────────────────────┘└────────────────────────┘└──
316 revert x,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────────────┘└─
317 rw ← succ_pred i h,
id └───────┘ ┴ ┴
src └───┘└───────┘┴ ┴
typ └───┘└───────┘┴┴┴┴
doc └───┘ ┴ ┴
txt └───┘ ┴ ┴
par └───┘ ┴ ┴
pid └─┘ ┴ ┴
st ───────────────────────┘└─
318 assume x,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────────┘└─
319 rw [tail_update_succ, tail_update_succ, map_smul] }
id └──────────────┘ └──────────────┘ └──────┘
src └──┘└──────────────┘└┘└──────────────┘└┘└──────┘└┘
typ └──┘└──────────────┘└┘└──────────────┘└┘└──────┘└┘
doc └──┘└──────────────┘└┘└──────────────┘└┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ─────────────────────────┘└────────────────┘└────────┘┴┴└─
320 end }
st ────┘
321
322 @[simp] lemma linear_map.uncurry_left_apply
doc └──┘
323 (f : M 0 →ₗ[R] (multilinear_map R (λ(i : fin n), M i.succ) M₂)) (m : Πi, M i) :
id ┴ └─┘┴┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ └┘ ┴ ┴ ┴
src └─┘ ┴ └─────────────┘ └─┘ └───┘
typ ┴ └─┘┴┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ └┘ ┴ ┴ ┴
doc └─────────────┘
324 f.uncurry_left m = f (m 0) (tail m) := rfl
id ┴└───────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘
src └───────────┘ ┴ └──┘ └─┘
typ ┴└───────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘
doc └───────────┘ └──┘
325
326 /-- Given a multilinear map `f` in `n+1` variables, split the first variable to obtain
327 a linear map into multilinear maps in `n` variables, given by `x ↦ (m ↦ f (cons x m))`. -/
328 def multilinear_map.curry_left
329 (f : multilinear_map R M M₂) :
id └─────────────┘ ┴ ┴ └┘
src └─────────────┘
typ └─────────────┘ ┴ ┴ └┘
doc └─────────────┘
330 M 0 →ₗ[R] (multilinear_map R (λ(i : fin n), M i.succ) M₂) :=
id ┴ └─┘┴┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ └┘
src └─┘ ┴ └─────────────┘ └─┘ └───┘
typ ┴ └─┘┴┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ └┘
doc └─────────────┘
331 { to_fun := λx,
id ┴
typ ┴
332 { to_fun := λm, f (cons x m),
id ┴ ┴ └──┘ ┴ ┴
src └──┘
typ ┴ ┴ └──┘ ┴ ┴
doc └──┘
333 add := λm i y y', by simp,
id ┴ ┴ ┴ └┘
src └──┘
typ ┴ ┴ ┴ └┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
334 smul := λm i y c, by simp },
id ┴ ┴ ┴ ┴
src └───┘
typ ┴ ┴ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
335 add := λx y, by { ext m, exact cons_add f m x y },
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └───┘ └────┘└──────┘┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └───┘ └────┘└──────┘┴┴┴┴┴┴┴┴┴
doc └───┘ └────┘└──────┘┴ ┴ ┴ ┴ ┴
txt └───┘ └────┘ ┴ ┴ ┴ ┴ ┴
par └───┘ └────┘ ┴ ┴ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴ ┴ ┴ ┴
st └──────┘└───────────────────────┘└┘
336 smul := λc x, by { ext m, exact cons_smul f m c x } }
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └───┘ └────┘└───────┘┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └───┘ └────┘└───────┘┴┴┴┴┴┴┴┴┴
doc └───┘ └────┘└───────┘┴ ┴ ┴ ┴ ┴
txt └───┘ └────┘ ┴ ┴ ┴ ┴ ┴
par └───┘ └────┘ ┴ ┴ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴ ┴ ┴ ┴
st └──────┘└────────────────────────┘└┘
337
338 @[simp] lemma multilinear_map.curry_left_apply
doc └──┘
339 (f : multilinear_map R M M₂) (x : M 0) (m : Π(i : fin n), M i.succ) :
id └─────────────┘ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴└───┘
src └─────────────┘ └─┘ └───┘
typ └─────────────┘ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴└───┘
doc └─────────────┘
340 f.curry_left x m = f (cons x m) := rfl
id ┴└─────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘
src └─────────┘ ┴ └──┘ └─┘
typ ┴└─────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘
doc └─────────┘ └──┘
341
342 @[simp] lemma linear_map.curry_uncurry_left
doc └──┘
343 (f : M 0 →ₗ[R] (multilinear_map R (λ(i : fin n), M i.succ) M₂)) :
id ┴ └─┘┴┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ └┘
src └─┘ ┴ └─────────────┘ └─┘ └───┘
typ ┴ └─┘┴┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ └┘
doc └─────────────┘
344 f.uncurry_left.curry_left = f :=
id ┴└───────────┘└─────────┘ ┴ ┴
src └───────────┘└─────────┘ ┴
typ ┴└───────────┘└─────────┘ ┴ ┴
doc └───────────┘└─────────┘
345 begin
st └─────
346 ext m x,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └──┘
st ────────┘└─
347 simp only [tail_cons, linear_map.uncurry_left_apply, multilinear_map.curry_left_apply],
id └───────┘ └───────────────────────────┘ └──────────────────────────────┘
src └─────────┘└───────┘└┘└───────────────────────────┘└┘└──────────────────────────────┘┴
typ └─────────┘└───────┘└┘└───────────────────────────┘└┘└──────────────────────────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
348 rw cons_zero
id └───────┘
src └─┘└───────┘┴
typ └─┘└───────┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ──────────────┘
349 end
st └─┘
350
351 @[simp] lemma multilinear_map.uncurry_curry_left
doc └──┘
352 (f : multilinear_map R M M₂) :
id └─────────────┘ ┴ ┴ └┘
src └─────────────┘
typ └─────────────┘ ┴ ┴ └┘
doc └─────────────┘
353 f.curry_left.uncurry_left = f :=
id ┴└─────────┘└───────────┘ ┴ ┴
src └─────────┘└───────────┘ ┴
typ ┴└─────────┘└───────────┘ ┴ ┴
doc └─────────┘└───────────┘
354 by { ext m, simp }
src └───┘ └───┘
typ └───┘ └───┘
doc └───┘ └───┘
txt └───┘ └───┘
par └───┘ └───┘
pid └┘ ┴
st └──────┘└─────┘└┘
355
356 variables (R M M₂)
357
358 /-- The space of multilinear maps on `Π(i : fin (n+1)), M i` is canonically isomorphic to
359 the space of linear maps from `M 0` to the space of multilinear maps on
360 `Π(i : fin n), M i.succ `, by separating the first variable. We register this isomorphism as a
361 linear isomorphism in `multilinear_curry_left_equiv R M M₂`.
362
363 The direct and inverse maps are given by `f.uncurry_left` and `f.curry_left`. Use these
364 unless you need the full framework of linear equivs. -/
365 def multilinear_curry_left_equiv :
366 (M 0 →ₗ[R] (multilinear_map R (λ(i : fin n), M i.succ) M₂)) ≃ₗ[R] (multilinear_map R M M₂) :=
id ┴ └─┘┴┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ └┘ └─┘┴┴ └─────────────┘ ┴ ┴ └┘
src └─┘ ┴ └─────────────┘ └─┘ └───┘ └─┘ ┴ └─────────────┘
typ ┴ └─┘┴┴ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ └┘ └─┘┴┴ └─────────────┘ ┴ ┴ └┘
doc └─────────────┘ └─┘ ┴ └─────────────┘
367 { to_fun := linear_map.uncurry_left,
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
doc └─────────────────────┘
368 add := λf₁ f₂, by { ext m, refl },
id └┘ └┘
src └───┘ └───┘
typ └┘ └┘ └───┘ └───┘
doc └───┘ └───┘
txt └───┘ └───┘
par └───┘ └───┘
pid └┘ ┴
st └──────┘└─────┘└┘
369 smul := λc f, by { ext m, refl },
id ┴ ┴
src └───┘ └───┘
typ ┴ ┴ └───┘ └───┘
doc └───┘ └───┘
txt └───┘ └───┘
par └───┘ └───┘
pid └┘ ┴
st └──────┘└─────┘└┘
370 inv_fun := multilinear_map.curry_left,
id └────────────────────────┘
src └────────────────────────┘
typ └────────────────────────┘
doc └────────────────────────┘
371 left_inv := linear_map.curry_uncurry_left,
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
372 right_inv := multilinear_map.uncurry_curry_left }
id └────────────────────────────────┘
src └────────────────────────────────┘
typ └────────────────────────────────┘
373
374 variables {R M M₂}
375
376 /-- Given a multilinear map `f` in `n` variables to the space of linear maps from `M 0` to `M₂`,
377 construct the corresponding multilinear map on `n+1` variables obtained by concatenating
378 the variables, given by `m ↦ f (tail m) (m 0)`-/
379 def multilinear_map.uncurry_right (f : (multilinear_map R (λ(i : fin n), M i.succ) ((M 0) →ₗ[R] M₂))) :
id └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ └┘
src └─────────────┘ └─┘ └───┘ └─┘ ┴
typ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ └┘
doc └─────────────┘
380 multilinear_map R M M₂ :=
id └─────────────┘ ┴ ┴ └┘
src └─────────────┘
typ └─────────────┘ ┴ ┴ └┘
doc └─────────────┘
381 { to_fun := λm, f (tail m) (m 0),
id ┴ ┴ └──┘ ┴ ┴
src └──┘
typ ┴ ┴ └──┘ ┴ ┴
doc └──┘
382 add := λm i x y, begin
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st └─────
383 by_cases h : i = 0,
id ┴ ┴
src └───────┘ └─┘ ┴┴└┘
typ └───────┘ └─┘┴┴┴└┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ─────────────────────┘└─
384 { revert x y,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ─────┘└────────┘└─
385 rw h,
id ┴
src └─┘
typ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────┘└─
386 assume x y,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────────────┘└─
387 rw [tail_update_zero, tail_update_zero, tail_update_zero, update_same,
id └──────────────┘ └──────────────┘ └──────────────┘ └─────────┘
src └──┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘└─────────┘└─
typ └──┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘└─────────┘└─
doc └──┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └─
st ─────────────────────────┘└────────────────┘└────────────────┘└───────────┘└─
388 update_same, update_same, linear_map.map_add] },
id └─────────┘ └─────────┘ └────────────────┘
src ─────────┘└─────────┘└┘└─────────┘└┘└────────────────┘└┘
typ ─────────┘└─────────┘└┘└─────────┘└┘└────────────────┘└┘
doc ─────────┘ └┘ └┘ └┘
txt ─────────┘ └┘ └┘ └┘
par ─────────┘ └┘ └┘ └┘
pid ─────────┘ └┘ └┘ ┴┴
st ────────────────────┘└───────────┘└──────────────────┘┴┴└┘└
389 { rw [update_noteq (ne.symm h), update_noteq (ne.symm h), update_noteq (ne.symm h)],
id └──────────┘ └─────┘ ┴ └──────────┘ └─────┘ ┴ └──────────┘ └─────┘ ┴
src └──┘└──────────┘┴ └─────┘┴ └─┘└──────────┘┴ └─────┘┴ └─┘└──────────┘┴ └─────┘┴ └┘
typ └──┘└──────────┘┴ └─────┘┴┴└─┘└──────────┘┴ └─────┘┴┴└─┘└──────────┘┴ └─────┘┴┴└┘
doc └──┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
txt └──┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
par └──┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
pid └┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
st ─────────────────────────────────┘└────────────────────────┘└────────────────────────┘└──
390 revert x y,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ───────────────┘└─
391 rw [← succ_pred i h],
id └───────┘ ┴ ┴
src └─────┘└───────┘┴ ┴ ┴
typ └─────┘└───────┘┴┴┴┴┴
doc └─────┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴
st ─────────────────────────┘└──
392 assume x y,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────────────┘└─
393 rw [tail_update_succ, map_add, tail_update_succ, tail_update_succ, linear_map.add_apply] }
id └──────────────┘
src └──┘└──────────────┘ └┘
typ └──┘└──────────────┘ └┘
doc └──┘└──────────────┘ └┘
txt └──┘ └┘
par └──┘ └┘
pid └┘ ┴┴
st ─────────────────────────┘ ┴┴└─
394 end,
st ────┘
395 smul := λm i c x, begin
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st └───┘
396 by_cases h : i = 0,
397 { revert x,
398 rw h,
399 assume x,
400 rw [update_same, update_same, tail_update_zero, tail_update_zero, linear_map.map_smul] },
src ┴
typ ┴
doc ┴
txt ┴
par ┴
pid ┴
st ┴ ┴
401 { rw [update_noteq (ne.symm h), update_noteq (ne.symm h)],
402 revert x,
403 rw [← succ_pred i h],
404 assume x,
405 rw [tail_update_succ, tail_update_succ, map_smul, linear_map.smul_apply] }
src ┴
typ ┴
doc ┴
txt ┴
par ┴
pid ┴
st ┴ └─
406 end }
st ────┘
407
408 @[simp] lemma multilinear_map.uncurry_right_apply
doc └──┘
409 (f : (multilinear_map R (λ(i : fin n), M i.succ) ((M 0) →ₗ[R] M₂))) (m : Πi, M i) :
id └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ └┘ ┴ ┴ ┴
src └─────────────┘ └─┘ └───┘ └─┘ ┴
typ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ └┘ ┴ ┴ ┴
doc └─────────────┘
410 f.uncurry_right m = f (tail m) (m 0) := rfl
id ┴└────────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘
src └────────────┘ ┴ └──┘ └─┘
typ ┴└────────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘
doc └────────────┘ └──┘
411
412 /-- Given a multilinear map `f` in `n+1` variables, split the first variable to obtain
413 a multilinear map in `n` variables taking values in linear maps from `M 0` to `M₂`, given by
414 `m ↦ (x ↦ f (cons x m))`. -/
415 def multilinear_map.curry_right (f : multilinear_map R M M₂) :
id └─────────────┘ ┴ ┴ └┘
src └─────────────┘
typ └─────────────┘ ┴ ┴ └┘
doc └─────────────┘
416 multilinear_map R (λ(i : fin n), M i.succ) ((M 0) →ₗ[R] M₂) :=
id └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ └┘
src └─────────────┘ └─┘ └───┘ └─┘ ┴
typ └─────────────┘ ┴ └─┘ ┴ ┴ ┴└───┘ ┴ └─┘┴┴ └┘
doc └─────────────┘
417 { to_fun := λm,
id ┴
typ ┴
418 { to_fun := λx, f (cons x m),
id ┴ ┴ └──┘ ┴ ┴
src └──┘
typ ┴ ┴ └──┘ ┴ ┴
doc └──┘
419 add := λx y, by rw f.cons_add,
id ┴ ┴
src └─┘
typ ┴ ┴ └─┘└┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └────┘
420 smul := λc x, by rw f.cons_smul },
id ┴ ┴
typ ┴ ┴
st ┴
421 add := λm i x y, begin
id ┴ ┴ ┴
typ ┴ ┴ ┴
422 ext z,
423 change f (cons z (update m i (x + y))) = f (cons z (update m i x)) + f (cons z (update m i y)),
id ┴
typ ┴
424 rw [cons_update, cons_update, cons_update, f.map_add]
st ┴
425 end,
st └─┘
426 smul := λm i c x, begin
id ┴ ┴ ┴
typ ┴ ┴ ┴
427 ext z,
428 change f (cons z (update m i (c • x))) = c • f (cons z (update m i x)),
id ┴ ┴
typ ┴ ┴
429 rw [cons_update, cons_update, f.map_smul]
st ┴
430 end }
st └─┘
431
432 @[simp] lemma multilinear_map.curry_right_apply
doc └──┘
433 (f : multilinear_map R M M₂) (x : M 0) (m : Π(i : fin n), M i.succ) :
id ┴ ┴ └┘ ┴ └┘ ┴ ┴
src └┘
typ ┴ ┴ └┘ ┴ └┘ ┴ ┴
434 f.curry_right m x = f (cons x m) := rfl
435
436 @[simp] lemma multilinear_map.curry_uncurry_right
doc └──┘
437 (f : (multilinear_map R (λ(i : fin n), M i.succ) ((M 0) →ₗ[R] M₂))) :
id ┴ └┘ ┴ ┴ ┴ └┘
src └┘
typ ┴ └┘ ┴ ┴ ┴ └┘
438 f.uncurry_right.curry_right = f :=
439 begin
440 ext m x,
441 simp only [cons_zero, multilinear_map.curry_right_apply, multilinear_map.uncurry_right_apply],
442 rw tail_cons
443 end
st └─┘
444
445 @[simp] lemma multilinear_map.uncurry_curry_right
doc └──┘
446 (f : multilinear_map R M M₂) :
id ┴ ┴ └┘
typ ┴ ┴ └┘
447 f.curry_right.uncurry_right = f :=
448 by { ext m, simp }
st └┘
449
450 variables (R M M₂)
451
452 /-- The space of multilinear maps on `Π(i : fin (n+1)), M i` is canonically isomorphic to
453 the space of linear maps from the space of multilinear maps on `Π(i : fin n), M i.succ` to the space of linear
454 maps on `M 0`, by separating the first variable. We register this isomorphism as a
455 linear isomorphism in `multilinear_curry_right_equiv R M M₂`.
456
457 The direct and inverse maps are given by `f.uncurry_right` and `f.curry_right`. Use these
458 unless you need the full framework of linear equivs. -/
459 def multilinear_curry_right_equiv :
460 (multilinear_map R (λ(i : fin n), M i.succ) ((M 0) →ₗ[R] M₂)) ≃ₗ[R] (multilinear_map R M M₂) :=
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘
src └┘
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘
461 { to_fun := multilinear_map.uncurry_right,
462 add := λf₁ f₂, by { ext m, refl },
st └┘
463 smul := λc f, by { ext m, rw [smul_apply], refl },
id ┴
typ ┴
st └┘
464 inv_fun := multilinear_map.curry_right,
465 left_inv := multilinear_map.curry_uncurry_right,
466 right_inv := multilinear_map.uncurry_curry_right }
467
468 end currying